package model.solver;

import java.io.BufferedWriter;
import java.io.IOException;

import model.ParameterValue;
import controller.solver.MiniSat;
import controller.xml.XMLBaliseFormat;

/**
 * Class for managing of {@link MiniSat} parameter.
 * 
 * @author GRONOWSKI Stephane svan001@aol.com
 * 
 *         igsat 2010
 * 
 */
public class MiniSatParameter extends SolverParameter {

	/** value "not used" for a parameter */
	public static final int		NOT_USED		= -4;
	/** minimal value of verbosity parameter */
	public static final int		MIN_VERBOSITY	= 0;
	/** maximal value of verbosity parameter */
	public static final int		MAX_VERBOSITY	= 2;
	/** minimal value of decay parameter */
	public static final double	MIN_DECAY		= 0;
	/** maximal value of decay parameter */
	public static final double	MAX_DECAY		= 1;
	/** minimal value of rnd-freq parameter */
	public static final double	MIN_RND_FREQ	= 0;
	/** maximal value of rnd-freq parameter */
	public static final double	MAX_RND_FREQ	= 1;

	private boolean				pre				= false;
	private ParameterValue		asymm			= ParameterValue.NOT_USED;
	private ParameterValue		rcheck			= ParameterValue.NOT_USED;
	private int					grow			= NOT_USED;
	private ParameterValue		polarityMode	= ParameterValue.NOT_USED;
	private double				decay			= NOT_USED;
	private double				rndfreq			= NOT_USED;
	private int					verbosity		= NOT_USED;

	/**
	 * Export the data in XML
	 * 
	 * @param file
	 *            {@link BufferedWriter} to write
	 * @throws IOException
	 */
	@Override
	public void exportXML(BufferedWriter file) throws IOException {
		// open
		// file.newLine();
		file.write("<" + XMLBaliseFormat.PARAMETER + " " + XMLBaliseFormat.TYPE_PARAMETER + "=" + "\""
				+ XMLBaliseFormat.TYPE_PARAMETER_SOLVEUR + "\"" + " >");

		// solver param
		super.exportXML(file);

		// pre
		// file.newLine();
		file.write("<" + XMLBaliseFormat.MINISAT_PRE + ">");
		if (pre)
			file.write(XMLBaliseFormat.TRUE);
		else
			file.write(XMLBaliseFormat.FALSE);
		file.write("</" + XMLBaliseFormat.MINISAT_PRE + ">");

		// asymm
		// file.newLine();
		file.write("<" + XMLBaliseFormat.MINISAT_ASYMM + ">");
		file.write(asymm.getXmlValue());
		file.write("</" + XMLBaliseFormat.MINISAT_ASYMM + ">");

		// rcheck
		// file.newLine();
		file.write("<" + XMLBaliseFormat.MINISAT_RECHECK + ">");
		file.write(rcheck.getXmlValue());
		file.write("</" + XMLBaliseFormat.MINISAT_RECHECK + ">");

		// grow
		// file.newLine();
		file.write("<" + XMLBaliseFormat.MINISAT_GROY + ">");
		file.write(String.valueOf(grow));
		file.write("</" + XMLBaliseFormat.MINISAT_GROY + ">");

		// polarity
		// file.newLine();
		file.write("<" + XMLBaliseFormat.MINISAT_POLARITY + ">");
		file.write(polarityMode.getXmlValue());
		file.write("</" + XMLBaliseFormat.MINISAT_POLARITY + ">");

		// decay
		// file.newLine();
		file.write("<" + XMLBaliseFormat.MINISAT_DECAY + ">");
		file.write(String.valueOf(decay));
		file.write("</" + XMLBaliseFormat.MINISAT_DECAY + ">");

		// rndfreq
		// file.newLine();
		file.write("<" + XMLBaliseFormat.MINISAT_RNDFREQ + ">");
		file.write(String.valueOf(rndfreq));
		file.write("</" + XMLBaliseFormat.MINISAT_RNDFREQ + ">");

		// verbosity
		// file.newLine();
		file.write("<" + XMLBaliseFormat.MINISAT_VERBOSITY + ">");
		file.write(String.valueOf(verbosity));
		file.write("</" + XMLBaliseFormat.MINISAT_VERBOSITY + ">");

		// close
		// file.newLine();
		file.write("</" + XMLBaliseFormat.PARAMETER + ">");
	}


	/**
	 * Return if it used satellite as preprocessor.
	 * 
	 * @return if it used satellite as preprocessor
	 */
	public boolean isPre() {
		return pre;
	}

	/**
	 * Set to true if you want to use satellite as preprocessor.
	 * 
	 * @param pre
	 *            value.
	 */
	public void setPre(boolean pre) {
		this.pre = pre;
	}

	/**
	 * unknown parameter.
	 * 
	 * @return value
	 */
	public ParameterValue getAsymm() {
		return asymm;
	}

	/**
	 * @deprecated currently not used
	 * 
	 * @param asymm
	 *            doesn't matter ^^
	 */
	@Deprecated
	public void setAsymm(ParameterValue asymm) {
		// this.asymm = asymm;
	}

	/**
	 * Return the value of rcheck parameter.
	 * 
	 * @return the value of rcheck parameter.
	 */
	public ParameterValue getRcheck() {
		return rcheck;
	}

	/**
	 * Set checking for redundant clause.
	 * 
	 * @param rcheck
	 *            value
	 * @return if it works.
	 */
	public boolean setRcheck(ParameterValue rcheck) {
		if (rcheck == ParameterValue.RANDOM)
			return false;
		this.rcheck = rcheck;
		return true;
	}

	/**
	 * Return value of the grow parameter.
	 * 
	 * @return value of the grow parameter.
	 */
	public int getGrow() {
		return grow;
	}

	/**
	 * Set the number of clause that may be introduced when eliminating a variable.
	 * 
	 * @param grow
	 *            valuee
	 * @return if it works
	 */
	public boolean setGrow(int grow) {
		if (grow != NOT_USED && grow <= 0)
			return false;

		this.grow = grow;
		return true;
	}

	/**
	 * Return the value of the polarity mode parameter.
	 * 
	 * @return the value of the polarity mode parameter.
	 */
	public ParameterValue getPolarityMode() {
		return polarityMode;
	}

	/**
	 * Set the default polariy .
	 * 
	 * @param polarityMode
	 *            value.
	 */
	public void setPolarityMode(ParameterValue polarityMode) {
		this.polarityMode = polarityMode;
	}

	/**
	 * Return the value of the decay paramter.
	 * 
	 * @return the value of the decay paramter.
	 */
	public double getDecay() {
		return decay;
	}

	/**
	 * Set the variable activity decay factor.
	 * 
	 * @param decay
	 *            value.
	 * @return if it works.
	 */
	public boolean setDecay(double decay) {
		if (decay != NOT_USED && (decay > MAX_DECAY || decay < MIN_DECAY))
			return false;

		this.decay = decay;
		return true;
	}

	/**
	 * Return the rnd-freq parameter value.
	 * 
	 * @return the rnd-freq parameter value.
	 */
	public double getRndfreq() {
		return rndfreq;
	}

	/**
	 * Set frequency with witch the decision heuristic tries to choose a random variable.
	 * 
	 * @param rndfreq
	 *            value
	 * @return if it works.
	 */
	public boolean setRndfreq(double rndfreq) {
		if (rndfreq != NOT_USED && (rndfreq > MAX_RND_FREQ || rndfreq < MIN_RND_FREQ))
			return false;

		this.rndfreq = rndfreq;
		return true;

	}

	/**
	 * Return the verbosity parameter value.
	 * 
	 * @return the verbosity parameter value.
	 */
	public int getVerbosity() {
		return verbosity;
	}

	/**
	 * Set the verbosity.
	 * 
	 * @param verbosity
	 *            value
	 * @return if it works.
	 */
	public boolean setVerbosity(int verbosity) {
		if (verbosity != NOT_USED && (verbosity > MAX_VERBOSITY || verbosity < MIN_VERBOSITY))
			return false;

		this.verbosity = verbosity;
		return true;
	}

	/**
	 * Create new {@link MiniSatParameter} parameter.
	 */
	public MiniSatParameter() {
	}

	/**
	 * Create a {@link MiniSatParameter} parameter.
	 * 
	 * @param param
	 *            the {@link SolverParameter}
	 */
	public MiniSatParameter(SolverParameter param) {
		timeOut = param.getTimeOut();
	}

	@Override
	public boolean basicCheck() {
		if (!super.basicCheck())
			return false;

		if (rcheck == ParameterValue.RANDOM)
			return false;

		if (grow != NOT_USED && grow <= 0)
			return false;

		if (decay != NOT_USED && (decay > MAX_DECAY || decay < MIN_DECAY))
			return false;

		if (rndfreq != NOT_USED && (rndfreq > MAX_RND_FREQ || rndfreq < MIN_RND_FREQ))
			return false;

		if (verbosity != NOT_USED && (verbosity > MAX_VERBOSITY || verbosity < MIN_VERBOSITY))
			return false;

		return true;
	}

	/**
	 * Return the number of parameter that will be add in the command line giving the current
	 * parameter
	 * 
	 * @return the number of parameter that will be add in the command line giving the current
	 *         parameter
	 */
	public int getCommandLineNbParameterSup() {
		int nb = 1; // pre
		if (asymm != ParameterValue.NOT_USED)
			nb++;

		if (rcheck != ParameterValue.NOT_USED)
			nb++;

		if (grow != NOT_USED)
			nb++;

		if (polarityMode != ParameterValue.NOT_USED)
			nb++;

		if (decay != NOT_USED)
			nb++;

		if (rndfreq != NOT_USED)
			nb++;

		if (verbosity != NOT_USED)
			nb++;

		return nb;
	}

}
